A:Type, eq:EqDecider(A), B:(AType), f,g,h:fpf(A; a.B(a)).
fpf-compatible(A; a.B(a); eq; h; f)
 fpf-compatible(A; a.B(a); eq; h; g)
 fpf-compatible(A; a.B(a); eq; h; fpf-join(eq; f; g)) 

latex

Definitions	x:A. B(x), x(s), P  Q, fpf-compatible(A; a.B(a); eq; f; g), t  T, x. t(x), P  Q, P  Q, if b then t else f fi , P  Q, tt, ff, prop{i:l}, , Unit, A, P  Q, False,
Lemmas	fpf-compatible wf, fpf wf, deq wf, fpf-ap wf, fpf-join-ap, fpf-dom wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-trivial-subtype-top, fpf-join wf, top wf, fpf-join-dom